fix: bad-character shift in Boyer-Moore search has no effect - #15010
fix: bad-character shift in Boyer-Moore search has no effect#15010bolverk wants to merge 1 commit into
Conversation
Reassigning the for-loop variable in bad_character_heuristic() does not change Python iteration, so the bad-character shift was dead code and the search ran as brute force. Convert to a while loop so the shift advances the search, and compute the shift in the pattern's coordinate space. The revised algorithm is machine-verified with Dafny (soundness and completeness); it agrees with a brute-force scan on 30k random inputs.
algorithms-keeper
Bot
added
enhancement
daltino
left a comment
daltino
left a comment
There was a problem hiding this comment.
The fix itself is correct — reassigning a for-loop variable in Python is indeed a no-op and the while-loop rewrite is the right approach. That said, the diff is a bit hard to evaluate in isolation because it doesn't show the full updated implementation; I'd want to verify the shift calculation specifically: the bad-character shift should be max(1, mismatch_offset - last_occurrence) where last_occurrence is the rightmost index of the mismatched character in the pattern to the left of mismatch_offset — making sure it's clamped to at least 1 is critical to avoid an infinite loop when the character appears at or to the right of the mismatch position. It would also strengthen the PR significantly to add a test case that would have caught the original bug — something like asserting that a pattern search on a long string of repeated characters completes in sub-quadratic time or simply verifying correct positions are returned for a case where the bad-character shift should skip multiple positions at once.
3 participants
Fix bad-character shift having no effect (dead loop variable)
Fixes #14844
Summary
bad_character_heuristic()instrings/boyer_moore_search.pyassigned thecomputed shift to the
for-loop variablei:In Python, reassigning a
for-loop variable inside the loop body has no effecton the iteration sequence, so the shift was dead code and the search silently ran
as a plain O(n·m) scan over every position.
The rewrite uses a
whileloop so the shift actually advances the search, andcomputes the shift in the pattern's coordinate space (the mismatch offset and
the alignment target are both pattern indices), instead of mixing a text index
with a pattern index as the old code did.
Correctness
The new algorithm was first written in Dafny and machine-verified (15 proof
obligations, 0 errors machine-checked by the SMT-based verifier) to establish:
pattern.The key safety invariant is documented in the docstring: a jump maps the
mismatching text position onto a pattern index that carries a character unequal
to it, so no skipped alignment can be a match.
In addition to the proof, the implementation agrees with a brute-force scan on
30,000 randomized inputs (empty text, single-character and repeated patterns).
Impact (the issue's own reproduction)
text = "ABCDEFGHIJKLMNOPABCDEFGHIJKLMNOP",pattern = "MNOP":The existing doctest
BoyerMooreSearch("ABAABA", "AB").bad_character_heuristic()still returns
[0, 3].Checklist
ruff check,ruff format --check, and the doctests